g:IMonoid, b:, p, q:|g|. (when b. (p * q)) = ((when b. p) * (when b. q))  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, when b. p
Definitions	ff, tt, t  T, if b then t else f fi , when b. p, x:A. B(x), x f y, P  Q, P & Q, P  Q, P  Q, Unit, , IMonoid,
Lemmas	imon wf, bool wf, grp car wf, grp op wf, mon ident, grp id wf